$\forall$$i$:Id. es{-}real\{i:l\}(${\it es}$.@$i$ locl(mkid\{a:ut2\}) occurs once)